Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		from(X)	→ cons(X,n__from(s(X)))
2:		sel(0,cons(X,XS))	→ X
3:		sel(s(N),cons(X,XS))	→ sel(N,activate(XS))
4:		minus(X,0)	→ 0
5:		minus(s(X),s(Y))	→ minus(X,Y)
6:		quot(0,s(Y))	→ 0
7:		quot(s(X),s(Y))	→ s(quot(minus(X,Y),s(Y)))
8:		zWquot(XS,nil)	→ nil
9:		zWquot(nil,XS)	→ nil
10:		zWquot(cons(X,XS),cons(Y,YS))	→ cons(quot(X,Y),n__zWquot(activate(XS),activate(YS)))
11:		from(X)	→ n__from(X)
12:		zWquot(X1,X2)	→ n__zWquot(X1,X2)
13:		activate(n__from(X))	→ from(X)
14:		activate(n__zWquot(X1,X2))	→ zWquot(X1,X2)
15:		activate(X)	→ X

There are 10 dependency pairs:


16:		SEL(s(N),cons(X,XS))	→ SEL(N,activate(XS))
17:		SEL(s(N),cons(X,XS))	→ ACTIVATE(XS)
18:		MINUS(s(X),s(Y))	→ MINUS(X,Y)
19:		QUOT(s(X),s(Y))	→ QUOT(minus(X,Y),s(Y))
20:		QUOT(s(X),s(Y))	→ MINUS(X,Y)
21:		ZWQUOT(cons(X,XS),cons(Y,YS))	→ QUOT(X,Y)
22:		ZWQUOT(cons(X,XS),cons(Y,YS))	→ ACTIVATE(XS)
23:		ZWQUOT(cons(X,XS),cons(Y,YS))	→ ACTIVATE(YS)
24:		ACTIVATE(n__from(X))	→ FROM(X)
25:		ACTIVATE(n__zWquot(X1,X2))	→ ZWQUOT(X1,X2)

The approximated dependency graph contains 4 SCCs: {18}, {19}, {22,23,25} and {16}.

Consider the SCC {18}. There are no usable rules. By taking the AF π with π(MINUS) = 1 together with the lexicographic path order with empty precedence, rule 18 is strictly decreasing.

Consider the SCC {19}. The usable rules are {4,5}. By taking the AF π with π(QUOT) = 1 and π(minus) = π(s) = [ ] together with the lexicographic path order with precedence s ≻ minus ≻ 0, rule 5 is weakly decreasing and the rules in {4,19} are strictly decreasing.

Consider the SCC {22,23,25}. There are no usable rules. By taking the AF π with π(ACTIVATE) = 1 and π(cons) = 2 together with the lexicographic path order with precedence n__zWquot ≻ ZWQUOT, the rules in {22,23,25} are strictly decreasing.

Consider the SCC {16}. The usable rules are {1,4-15}. By taking the AF π with π(activate) = π(SEL) = 1, π(cons) = 2, π(from) = π(minus) = π(n__from) = π(n__zWquot) = π(zWquot) = [ ] and π(quot) = [1] together with the lexicographic path order with precedence n__zWquot ≻ nil, quot ≻ s ≻ minus ≻ 0, n__from ≈ from and n__zWquot ≈ zWquot, the rules in {1,5,10-15} are weakly decreasing and the rules in {4,6-9,16} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (1.75 seconds) --- May 4, 2006